The invention relates to technology for implementing electronic design automation tools, and in particular, design tools for performing simulation of electrical circuit designs.
An IC is a small electronic device typically formed from semiconductor material. Each IC contains a large number of electronic components that are wired together to create a self-contained circuit device. A single IC may include millions of individual devices, such as transistors, capacitors, and resistors, formed on a chip to perform desired functions.
Production of complex ICs is an intricate process that involves many steps. One of the first steps in producing an IC involves designing a virtual version of the IC using computer-aided design tools. The design of a virtual version of an IC can be broken down into three general areas: design definition, design verification, and design layout. IC design definition can be described at various levels of sophistication or detail. The levels of design sophistication include the functional level, also referred to as the register transfer level (RTL) or the architectural level; the logical level, also referred to as the gate level; and the transistor level, also referred to as the layout level.
Numerous approaches can be taken to perform design verification. Functional verification is an approach that verifies the functionality and operation of a circuit design. Two well known approaches to performing functional verification are circuit simulation and formal verification.
A circuit simulator is a software-driven system used to dynamically predict the behavior of electrical circuits or other physical systems. Given a description of a circuit and a stimulus, the simulator dynamically generates and outputs the response of the circuit to the stimulus. The stimulus includes “test vectors” that test the operation of the circuit design under a specified set of conditions. In conventional systems, random simulation is routinely used to verify the circuit design. Random simulation is generally based on the following three postulates: a) to prove that a design is correct by simulation one needs to test the design's behavior for all inputs; b) since the set of all inputs is huge, simulation cannot be complete; c) to increase the chances of hitting a bug one should “spray” test vectors more or less uniformly over the set of all possible inputs.
Formal verification is an algorithmic-based approach to logic verification that exhaustively proves functional properties about a design. Using a mathematical model of the circuit design, the formal verification process attempts to check that the circuit will properly function under all conditions.
Formal verification and simulation are the two extremes of functional verification. Formal verification guarantees that a property holds for all inputs but scales up poorly. In contrast, simulation scales up well but guarantees only that a property holds for the set of generated test inputs.
To address the flaws in circuit simulation, there are approaches to curb the “randomness” of generated tests. One method is to bias random values assigned to a particular variable. To introduce biases “dynamically”, markov chains may be used. Another way to reduce randomness is to add to the design under test some constraints and require that every test vector satisfies the constraints. These constraints can be of different nature. For example, they may describe design's environment or specify some scenario under which the design needs to be tested. One significant problem with these approaches is that they cannot guarantee complete coverage of a particular part of the search space. Moreover, they are not very effective at taking into account design specifics and cannot be used to smoothly change the ratio of deterministic and random components of simulation.
Embodiments of the present invention are directed to an improved verification approach that simultaneously provides the coverage advantage of formal verification with the scaling efficiencies of simulation. Some embodiments of the invention provide a method and system for generating an “intelligent” set of test vectors off a resolution proof. The intelligent set of test vectors, which do not need to be random, can be used to simulate the circuit design with dramatically higher coverage.